$\forall$${\it es}$:ES, $T$:Type, $I$:MaInterface($T$), $i$:Id.
\\[0ex]ma{-}interface{-}consistent(${\it es}$;$I$) $\Rightarrow$ ($i$ $\in$ ma{-}interface{-}locs($I$)) $\Rightarrow$ ([[$I$$\mid$$i$]] $\in$ AbsInterface($T$))